(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 5))
(let ((e5 3))
(let ((e6 (/ e5 e5)))
(let ((e7 (* v2 v2)))
(let ((e8 (- v0)))
(let ((e9 (- e7 e8)))
(let ((e10 (- v2)))
(let ((e11 (- e7 e7)))
(let ((e12 (* e3 e6)))
(let ((e13 (- e7 e12)))
(let ((e14 (* e10 e7)))
(let ((e15 (* e9 e9)))
(let ((e16 (- e11 e9)))
(let ((e17 (- e8)))
(let ((e18 (- e12)))
(let ((e19 (- e9)))
(let ((e20 (+ v1 e15)))
(let ((e21 (* e13 e8)))
(let ((e22 (- e6 v2)))
(let ((e23 (/ e5 e5)))
(let ((e24 (+ e14 e19)))
(let ((e25 (- e24)))
(let ((e26 (+ e25 v0)))
(let ((e27 (- e25 e12)))
(let ((e28 (* e20 e21)))
(let ((e29 (* e8 e11)))
(let ((e30 (- e11)))
(let ((e31 (- v2 e29)))
(let ((e32 (* e30 e29)))
(let ((e33 (- e25 e11)))
(let ((e34 (- e18)))
(let ((e35 (/ e5 e4)))
(let ((e36 (< e9 e7)))
(let ((e37 (<= e10 e15)))
(let ((e38 (> e21 e11)))
(let ((e39 (<= e21 e28)))
(let ((e40 (>= e9 e27)))
(let ((e41 (>= e27 e15)))
(let ((e42 (distinct e10 e19)))
(let ((e43 (distinct e6 e12)))
(let ((e44 (> e20 e11)))
(let ((e45 (< e17 e25)))
(let ((e46 (= e14 e28)))
(let ((e47 (> e29 e26)))
(let ((e48 (= v0 e23)))
(let ((e49 (> e26 e20)))
(let ((e50 (<= e11 e11)))
(let ((e51 (distinct v1 e31)))
(let ((e52 (> e22 e17)))
(let ((e53 (<= e26 e27)))
(let ((e54 (<= e13 e32)))
(let ((e55 (< e22 e29)))
(let ((e56 (> e10 e13)))
(let ((e57 (distinct v1 e33)))
(let ((e58 (< v2 e32)))
(let ((e59 (> e26 e30)))
(let ((e60 (<= e17 e24)))
(let ((e61 (= e8 e30)))
(let ((e62 (distinct e8 e8)))
(let ((e63 (= e31 e10)))
(let ((e64 (>= e6 e31)))
(let ((e65 (= e10 e9)))
(let ((e66 (= e16 e12)))
(let ((e67 (< e6 e7)))
(let ((e68 (distinct e22 e24)))
(let ((e69 (>= e22 e22)))
(let ((e70 (>= e15 e27)))
(let ((e71 (< e9 e33)))
(let ((e72 (>= e8 e16)))
(let ((e73 (= e20 e27)))
(let ((e74 (> e23 e33)))
(let ((e75 (<= v0 e28)))
(let ((e76 (< e31 e19)))
(let ((e77 (> e32 e33)))
(let ((e78 (>= e11 e13)))
(let ((e79 (> e28 e8)))
(let ((e80 (<= e8 e13)))
(let ((e81 (>= e31 e22)))
(let ((e82 (>= e12 e8)))
(let ((e83 (= e35 e12)))
(let ((e84 (> e31 e7)))
(let ((e85 (<= e24 e16)))
(let ((e86 (<= e24 e31)))
(let ((e87 (distinct e28 e18)))
(let ((e88 (> e33 e10)))
(let ((e89 (<= e13 e10)))
(let ((e90 (>= e7 e20)))
(let ((e91 (distinct e32 e29)))
(let ((e92 (>= e23 v0)))
(let ((e93 (distinct e30 e19)))
(let ((e94 (> v2 e25)))
(let ((e95 (>= e33 e31)))
(let ((e96 (> e22 e28)))
(let ((e97 (>= e32 e13)))
(let ((e98 (>= e11 e29)))
(let ((e99 (= e18 e21)))
(let ((e100 (> e8 e10)))
(let ((e101 (< e9 e7)))
(let ((e102 (> e32 v2)))
(let ((e103 (= e27 e11)))
(let ((e104 (> e33 e21)))
(let ((e105 (= e12 e16)))
(let ((e106 (= e33 v0)))
(let ((e107 (< v2 e33)))
(let ((e108 (> e32 e34)))
(let ((e109 (>= e35 e12)))
(let ((e110 (> e26 e12)))
(let ((e111 (< e15 e14)))
(let ((e112 (<= e19 e7)))
(let ((e113 (distinct e10 e9)))
(let ((e114 (< e21 e17)))
(let ((e115 (> e35 v2)))
(let ((e116 (<= e12 e7)))
(let ((e117 (> e10 e17)))
(let ((e118 (= e11 e26)))
(let ((e119 (> e17 e18)))
(let ((e120 (<= e11 e31)))
(let ((e121 (distinct e32 v0)))
(let ((e122 (> v1 e35)))
(let ((e123 (>= e22 e21)))
(let ((e124 (< e27 v0)))
(let ((e125 (>= v2 e24)))
(let ((e126 (> v2 v0)))
(let ((e127 (< e23 e26)))
(let ((e128 (>= e14 e10)))
(let ((e129 (< e32 e32)))
(let ((e130 (<= e12 e12)))
(let ((e131 (<= e7 e17)))
(let ((e132 (<= e23 e8)))
(let ((e133 (distinct e6 e10)))
(let ((e134 (= e18 v2)))
(let ((e135 (>= e34 e22)))
(let ((e136 (= e27 e16)))
(let ((e137 (> e9 v1)))
(let ((e138 (< e28 e7)))
(let ((e139 (>= e33 e26)))
(let ((e140 (>= e32 e32)))
(let ((e141 (<= e25 e17)))
(let ((e142 (> e22 e7)))
(let ((e143 (distinct e24 e18)))
(let ((e144 (> e33 e35)))
(let ((e145 (= e21 e31)))
(let ((e146 (> e14 e24)))
(let ((e147 (distinct v0 e13)))
(let ((e148 (= e28 e34)))
(let ((e149 (>= v2 e33)))
(let ((e150 (> e24 v2)))
(let ((e151 (< e6 e29)))
(let ((e152 (= e27 e9)))
(let ((e153 (>= e23 e8)))
(let ((e154 (distinct e23 e18)))
(let ((e155 (>= e6 e18)))
(let ((e156 (distinct e27 e14)))
(let ((e157 (<= e17 e21)))
(let ((e158 (<= e11 e31)))
(let ((e159 (distinct e15 e10)))
(let ((e160 (> e7 e14)))
(let ((e161 (< e7 e9)))
(let ((e162 (= e18 e26)))
(let ((e163 (< e8 e23)))
(let ((e164 (distinct e12 v0)))
(let ((e165 (distinct e16 e22)))
(let ((e166 (>= e28 e29)))
(let ((e167 (= e18 e29)))
(let ((e168 (>= e6 e6)))
(let ((e169 (distinct e10 e30)))
(let ((e170 (= e27 e28)))
(let ((e171 (<= e34 v2)))
(let ((e172 (distinct e14 e29)))
(let ((e173 (distinct e27 e8)))
(let ((e174 (distinct e17 e27)))
(let ((e175 (<= e11 e26)))
(let ((e176 (= e30 e35)))
(let ((e177 (= e31 e23)))
(let ((e178 (<= e20 e23)))
(let ((e179 (=> e41 e133)))
(let ((e180 (or e91 e107)))
(let ((e181 (=> e36 e62)))
(let ((e182 (and e78 e43)))
(let ((e183 (xor e109 e79)))
(let ((e184 (xor e152 e170)))
(let ((e185 (ite e154 e47 e59)))
(let ((e186 (and e58 e63)))
(let ((e187 (=> e100 e90)))
(let ((e188 (not e53)))
(let ((e189 (or e88 e46)))
(let ((e190 (ite e112 e148 e57)))
(let ((e191 (xor e121 e67)))
(let ((e192 (=> e151 e127)))
(let ((e193 (xor e183 e106)))
(let ((e194 (xor e153 e83)))
(let ((e195 (and e166 e85)))
(let ((e196 (xor e55 e163)))
(let ((e197 (not e157)))
(let ((e198 (xor e97 e180)))
(let ((e199 (or e145 e44)))
(let ((e200 (=> e104 e136)))
(let ((e201 (xor e74 e66)))
(let ((e202 (=> e61 e194)))
(let ((e203 (= e199 e147)))
(let ((e204 (and e176 e120)))
(let ((e205 (= e118 e39)))
(let ((e206 (=> e190 e87)))
(let ((e207 (and e131 e195)))
(let ((e208 (or e206 e40)))
(let ((e209 (not e71)))
(let ((e210 (and e156 e158)))
(let ((e211 (or e94 e49)))
(let ((e212 (or e203 e188)))
(let ((e213 (= e80 e56)))
(let ((e214 (not e189)))
(let ((e215 (=> e193 e214)))
(let ((e216 (xor e60 e175)))
(let ((e217 (and e123 e205)))
(let ((e218 (xor e213 e161)))
(let ((e219 (= e201 e38)))
(let ((e220 (=> e168 e186)))
(let ((e221 (not e48)))
(let ((e222 (not e122)))
(let ((e223 (ite e220 e84 e70)))
(let ((e224 (not e219)))
(let ((e225 (xor e72 e105)))
(let ((e226 (ite e191 e149 e198)))
(let ((e227 (or e128 e196)))
(let ((e228 (ite e42 e165 e143)))
(let ((e229 (or e223 e185)))
(let ((e230 (or e140 e173)))
(let ((e231 (= e51 e37)))
(let ((e232 (ite e117 e126 e208)))
(let ((e233 (= e177 e216)))
(let ((e234 (or e222 e218)))
(let ((e235 (=> e50 e113)))
(let ((e236 (xor e210 e134)))
(let ((e237 (or e92 e54)))
(let ((e238 (and e124 e86)))
(let ((e239 (ite e81 e45 e197)))
(let ((e240 (= e211 e182)))
(let ((e241 (not e125)))
(let ((e242 (= e139 e238)))
(let ((e243 (or e141 e89)))
(let ((e244 (= e212 e187)))
(let ((e245 (=> e221 e68)))
(let ((e246 (= e64 e237)))
(let ((e247 (and e115 e181)))
(let ((e248 (xor e162 e192)))
(let ((e249 (= e229 e102)))
(let ((e250 (xor e138 e111)))
(let ((e251 (not e164)))
(let ((e252 (and e249 e231)))
(let ((e253 (not e146)))
(let ((e254 (ite e252 e242 e184)))
(let ((e255 (and e240 e132)))
(let ((e256 (or e75 e171)))
(let ((e257 (not e225)))
(let ((e258 (xor e172 e241)))
(let ((e259 (and e65 e65)))
(let ((e260 (not e215)))
(let ((e261 (= e232 e247)))
(let ((e262 (=> e239 e248)))
(let ((e263 (xor e228 e99)))
(let ((e264 (xor e69 e129)))
(let ((e265 (or e262 e135)))
(let ((e266 (xor e207 e200)))
(let ((e267 (and e266 e204)))
(let ((e268 (not e155)))
(let ((e269 (=> e257 e202)))
(let ((e270 (ite e160 e174 e108)))
(let ((e271 (ite e179 e110 e255)))
(let ((e272 (not e103)))
(let ((e273 (ite e251 e209 e169)))
(let ((e274 (not e253)))
(let ((e275 (or e217 e272)))
(let ((e276 (= e235 e77)))
(let ((e277 (or e274 e230)))
(let ((e278 (= e159 e260)))
(let ((e279 (or e261 e142)))
(let ((e280 (xor e150 e270)))
(let ((e281 (ite e167 e236 e259)))
(let ((e282 (=> e273 e144)))
(let ((e283 (=> e277 e254)))
(let ((e284 (=> e250 e268)))
(let ((e285 (=> e96 e267)))
(let ((e286 (xor e258 e178)))
(let ((e287 (ite e224 e283 e98)))
(let ((e288 (=> e281 e226)))
(let ((e289 (xor e269 e279)))
(let ((e290 (xor e280 e271)))
(let ((e291 (xor e287 e276)))
(let ((e292 (=> e137 e256)))
(let ((e293 (= e95 e243)))
(let ((e294 (not e245)))
(let ((e295 (and e289 e227)))
(let ((e296 (xor e130 e119)))
(let ((e297 (=> e292 e282)))
(let ((e298 (= e278 e73)))
(let ((e299 (and e116 e265)))
(let ((e300 (or e286 e284)))
(let ((e301 (ite e93 e76 e293)))
(let ((e302 (=> e263 e288)))
(let ((e303 (not e275)))
(let ((e304 (= e246 e52)))
(let ((e305 (xor e300 e297)))
(let ((e306 (xor e264 e82)))
(let ((e307 (ite e295 e296 e285)))
(let ((e308 (and e294 e304)))
(let ((e309 (=> e114 e307)))
(let ((e310 (not e101)))
(let ((e311 (or e302 e290)))
(let ((e312 (not e310)))
(let ((e313 (and e303 e291)))
(let ((e314 (not e311)))
(let ((e315 (xor e299 e298)))
(let ((e316 (or e312 e309)))
(let ((e317 (xor e316 e316)))
(let ((e318 (ite e313 e233 e305)))
(let ((e319 (xor e234 e308)))
(let ((e320 (xor e318 e315)))
(let ((e321 (=> e306 e319)))
(let ((e322 (and e320 e321)))
(let ((e323 (ite e322 e314 e244)))
(let ((e324 (or e317 e317)))
(let ((e325 (=> e323 e324)))
(let ((e326 (xor e301 e325)))
e326
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
